0 Prolog
↳1 PrologToPrologProblemTransformerProof (⇒, 88 ms)
↳2 Prolog
↳3 PrologToPiTRSProof (⇒, 0 ms)
↳4 PiTRS
↳5 DependencyPairsProof (⇔, 26 ms)
↳6 PiDP
↳7 DependencyGraphProof (⇔, 0 ms)
↳8 AND
↳9 PiDP
↳10 UsableRulesProof (⇔, 0 ms)
↳11 PiDP
↳12 PiDPToQDPProof (⇒, 9 ms)
↳13 QDP
↳14 QDPSizeChangeProof (⇔, 0 ms)
↳15 YES
↳16 PiDP
↳17 UsableRulesProof (⇔, 0 ms)
↳18 PiDP
↳19 PiDPToQDPProof (⇒, 0 ms)
↳20 QDP
↳21 QDPSizeChangeProof (⇔, 0 ms)
↳22 YES
preorderC_in_ga(T5, T7) → U7_ga(T5, T7, preorder_dlA_in_ga(T5, T7))
preorder_dlA_in_ga(nil, []) → preorder_dlA_out_ga(nil, [])
preorder_dlA_in_ga(tree(T21, T22, T23), .(T22, T25)) → U1_ga(T21, T22, T23, T25, preorder_dlB_in_gaa(T21, T25, X26))
preorder_dlB_in_gaa(nil, T35, T35) → preorder_dlB_out_gaa(nil, T35, T35)
preorder_dlB_in_gaa(tree(T44, T45, T46), .(T45, T48), X55) → U4_gaa(T44, T45, T46, T48, X55, preorder_dlB_in_gaa(T44, T48, X54))
preorder_dlB_in_gaa(tree(T44, T45, T46), .(T45, T48), X55) → U5_gaa(T44, T45, T46, T48, X55, preorder_dlB_in_gaa(T44, T48, T51))
U5_gaa(T44, T45, T46, T48, X55, preorder_dlB_out_gaa(T44, T48, T51)) → U6_gaa(T44, T45, T46, T48, X55, preorder_dlB_in_gaa(T46, T51, X55))
U6_gaa(T44, T45, T46, T48, X55, preorder_dlB_out_gaa(T46, T51, X55)) → preorder_dlB_out_gaa(tree(T44, T45, T46), .(T45, T48), X55)
U4_gaa(T44, T45, T46, T48, X55, preorder_dlB_out_gaa(T44, T48, X54)) → preorder_dlB_out_gaa(tree(T44, T45, T46), .(T45, T48), X55)
U1_ga(T21, T22, T23, T25, preorder_dlB_out_gaa(T21, T25, X26)) → preorder_dlA_out_ga(tree(T21, T22, T23), .(T22, T25))
preorder_dlA_in_ga(tree(T21, T22, T23), .(T22, T25)) → U2_ga(T21, T22, T23, T25, preorder_dlB_in_gaa(T21, T25, T28))
U2_ga(T21, T22, T23, T25, preorder_dlB_out_gaa(T21, T25, T28)) → U3_ga(T21, T22, T23, T25, preorder_dlA_in_ga(T23, T28))
U3_ga(T21, T22, T23, T25, preorder_dlA_out_ga(T23, T28)) → preorder_dlA_out_ga(tree(T21, T22, T23), .(T22, T25))
U7_ga(T5, T7, preorder_dlA_out_ga(T5, T7)) → preorderC_out_ga(T5, T7)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
preorderC_in_ga(T5, T7) → U7_ga(T5, T7, preorder_dlA_in_ga(T5, T7))
preorder_dlA_in_ga(nil, []) → preorder_dlA_out_ga(nil, [])
preorder_dlA_in_ga(tree(T21, T22, T23), .(T22, T25)) → U1_ga(T21, T22, T23, T25, preorder_dlB_in_gaa(T21, T25, X26))
preorder_dlB_in_gaa(nil, T35, T35) → preorder_dlB_out_gaa(nil, T35, T35)
preorder_dlB_in_gaa(tree(T44, T45, T46), .(T45, T48), X55) → U4_gaa(T44, T45, T46, T48, X55, preorder_dlB_in_gaa(T44, T48, X54))
preorder_dlB_in_gaa(tree(T44, T45, T46), .(T45, T48), X55) → U5_gaa(T44, T45, T46, T48, X55, preorder_dlB_in_gaa(T44, T48, T51))
U5_gaa(T44, T45, T46, T48, X55, preorder_dlB_out_gaa(T44, T48, T51)) → U6_gaa(T44, T45, T46, T48, X55, preorder_dlB_in_gaa(T46, T51, X55))
U6_gaa(T44, T45, T46, T48, X55, preorder_dlB_out_gaa(T46, T51, X55)) → preorder_dlB_out_gaa(tree(T44, T45, T46), .(T45, T48), X55)
U4_gaa(T44, T45, T46, T48, X55, preorder_dlB_out_gaa(T44, T48, X54)) → preorder_dlB_out_gaa(tree(T44, T45, T46), .(T45, T48), X55)
U1_ga(T21, T22, T23, T25, preorder_dlB_out_gaa(T21, T25, X26)) → preorder_dlA_out_ga(tree(T21, T22, T23), .(T22, T25))
preorder_dlA_in_ga(tree(T21, T22, T23), .(T22, T25)) → U2_ga(T21, T22, T23, T25, preorder_dlB_in_gaa(T21, T25, T28))
U2_ga(T21, T22, T23, T25, preorder_dlB_out_gaa(T21, T25, T28)) → U3_ga(T21, T22, T23, T25, preorder_dlA_in_ga(T23, T28))
U3_ga(T21, T22, T23, T25, preorder_dlA_out_ga(T23, T28)) → preorder_dlA_out_ga(tree(T21, T22, T23), .(T22, T25))
U7_ga(T5, T7, preorder_dlA_out_ga(T5, T7)) → preorderC_out_ga(T5, T7)
PREORDERC_IN_GA(T5, T7) → U7_GA(T5, T7, preorder_dlA_in_ga(T5, T7))
PREORDERC_IN_GA(T5, T7) → PREORDER_DLA_IN_GA(T5, T7)
PREORDER_DLA_IN_GA(tree(T21, T22, T23), .(T22, T25)) → U1_GA(T21, T22, T23, T25, preorder_dlB_in_gaa(T21, T25, X26))
PREORDER_DLA_IN_GA(tree(T21, T22, T23), .(T22, T25)) → PREORDER_DLB_IN_GAA(T21, T25, X26)
PREORDER_DLB_IN_GAA(tree(T44, T45, T46), .(T45, T48), X55) → U4_GAA(T44, T45, T46, T48, X55, preorder_dlB_in_gaa(T44, T48, X54))
PREORDER_DLB_IN_GAA(tree(T44, T45, T46), .(T45, T48), X55) → PREORDER_DLB_IN_GAA(T44, T48, X54)
PREORDER_DLB_IN_GAA(tree(T44, T45, T46), .(T45, T48), X55) → U5_GAA(T44, T45, T46, T48, X55, preorder_dlB_in_gaa(T44, T48, T51))
U5_GAA(T44, T45, T46, T48, X55, preorder_dlB_out_gaa(T44, T48, T51)) → U6_GAA(T44, T45, T46, T48, X55, preorder_dlB_in_gaa(T46, T51, X55))
U5_GAA(T44, T45, T46, T48, X55, preorder_dlB_out_gaa(T44, T48, T51)) → PREORDER_DLB_IN_GAA(T46, T51, X55)
PREORDER_DLA_IN_GA(tree(T21, T22, T23), .(T22, T25)) → U2_GA(T21, T22, T23, T25, preorder_dlB_in_gaa(T21, T25, T28))
U2_GA(T21, T22, T23, T25, preorder_dlB_out_gaa(T21, T25, T28)) → U3_GA(T21, T22, T23, T25, preorder_dlA_in_ga(T23, T28))
U2_GA(T21, T22, T23, T25, preorder_dlB_out_gaa(T21, T25, T28)) → PREORDER_DLA_IN_GA(T23, T28)
preorderC_in_ga(T5, T7) → U7_ga(T5, T7, preorder_dlA_in_ga(T5, T7))
preorder_dlA_in_ga(nil, []) → preorder_dlA_out_ga(nil, [])
preorder_dlA_in_ga(tree(T21, T22, T23), .(T22, T25)) → U1_ga(T21, T22, T23, T25, preorder_dlB_in_gaa(T21, T25, X26))
preorder_dlB_in_gaa(nil, T35, T35) → preorder_dlB_out_gaa(nil, T35, T35)
preorder_dlB_in_gaa(tree(T44, T45, T46), .(T45, T48), X55) → U4_gaa(T44, T45, T46, T48, X55, preorder_dlB_in_gaa(T44, T48, X54))
preorder_dlB_in_gaa(tree(T44, T45, T46), .(T45, T48), X55) → U5_gaa(T44, T45, T46, T48, X55, preorder_dlB_in_gaa(T44, T48, T51))
U5_gaa(T44, T45, T46, T48, X55, preorder_dlB_out_gaa(T44, T48, T51)) → U6_gaa(T44, T45, T46, T48, X55, preorder_dlB_in_gaa(T46, T51, X55))
U6_gaa(T44, T45, T46, T48, X55, preorder_dlB_out_gaa(T46, T51, X55)) → preorder_dlB_out_gaa(tree(T44, T45, T46), .(T45, T48), X55)
U4_gaa(T44, T45, T46, T48, X55, preorder_dlB_out_gaa(T44, T48, X54)) → preorder_dlB_out_gaa(tree(T44, T45, T46), .(T45, T48), X55)
U1_ga(T21, T22, T23, T25, preorder_dlB_out_gaa(T21, T25, X26)) → preorder_dlA_out_ga(tree(T21, T22, T23), .(T22, T25))
preorder_dlA_in_ga(tree(T21, T22, T23), .(T22, T25)) → U2_ga(T21, T22, T23, T25, preorder_dlB_in_gaa(T21, T25, T28))
U2_ga(T21, T22, T23, T25, preorder_dlB_out_gaa(T21, T25, T28)) → U3_ga(T21, T22, T23, T25, preorder_dlA_in_ga(T23, T28))
U3_ga(T21, T22, T23, T25, preorder_dlA_out_ga(T23, T28)) → preorder_dlA_out_ga(tree(T21, T22, T23), .(T22, T25))
U7_ga(T5, T7, preorder_dlA_out_ga(T5, T7)) → preorderC_out_ga(T5, T7)
PREORDERC_IN_GA(T5, T7) → U7_GA(T5, T7, preorder_dlA_in_ga(T5, T7))
PREORDERC_IN_GA(T5, T7) → PREORDER_DLA_IN_GA(T5, T7)
PREORDER_DLA_IN_GA(tree(T21, T22, T23), .(T22, T25)) → U1_GA(T21, T22, T23, T25, preorder_dlB_in_gaa(T21, T25, X26))
PREORDER_DLA_IN_GA(tree(T21, T22, T23), .(T22, T25)) → PREORDER_DLB_IN_GAA(T21, T25, X26)
PREORDER_DLB_IN_GAA(tree(T44, T45, T46), .(T45, T48), X55) → U4_GAA(T44, T45, T46, T48, X55, preorder_dlB_in_gaa(T44, T48, X54))
PREORDER_DLB_IN_GAA(tree(T44, T45, T46), .(T45, T48), X55) → PREORDER_DLB_IN_GAA(T44, T48, X54)
PREORDER_DLB_IN_GAA(tree(T44, T45, T46), .(T45, T48), X55) → U5_GAA(T44, T45, T46, T48, X55, preorder_dlB_in_gaa(T44, T48, T51))
U5_GAA(T44, T45, T46, T48, X55, preorder_dlB_out_gaa(T44, T48, T51)) → U6_GAA(T44, T45, T46, T48, X55, preorder_dlB_in_gaa(T46, T51, X55))
U5_GAA(T44, T45, T46, T48, X55, preorder_dlB_out_gaa(T44, T48, T51)) → PREORDER_DLB_IN_GAA(T46, T51, X55)
PREORDER_DLA_IN_GA(tree(T21, T22, T23), .(T22, T25)) → U2_GA(T21, T22, T23, T25, preorder_dlB_in_gaa(T21, T25, T28))
U2_GA(T21, T22, T23, T25, preorder_dlB_out_gaa(T21, T25, T28)) → U3_GA(T21, T22, T23, T25, preorder_dlA_in_ga(T23, T28))
U2_GA(T21, T22, T23, T25, preorder_dlB_out_gaa(T21, T25, T28)) → PREORDER_DLA_IN_GA(T23, T28)
preorderC_in_ga(T5, T7) → U7_ga(T5, T7, preorder_dlA_in_ga(T5, T7))
preorder_dlA_in_ga(nil, []) → preorder_dlA_out_ga(nil, [])
preorder_dlA_in_ga(tree(T21, T22, T23), .(T22, T25)) → U1_ga(T21, T22, T23, T25, preorder_dlB_in_gaa(T21, T25, X26))
preorder_dlB_in_gaa(nil, T35, T35) → preorder_dlB_out_gaa(nil, T35, T35)
preorder_dlB_in_gaa(tree(T44, T45, T46), .(T45, T48), X55) → U4_gaa(T44, T45, T46, T48, X55, preorder_dlB_in_gaa(T44, T48, X54))
preorder_dlB_in_gaa(tree(T44, T45, T46), .(T45, T48), X55) → U5_gaa(T44, T45, T46, T48, X55, preorder_dlB_in_gaa(T44, T48, T51))
U5_gaa(T44, T45, T46, T48, X55, preorder_dlB_out_gaa(T44, T48, T51)) → U6_gaa(T44, T45, T46, T48, X55, preorder_dlB_in_gaa(T46, T51, X55))
U6_gaa(T44, T45, T46, T48, X55, preorder_dlB_out_gaa(T46, T51, X55)) → preorder_dlB_out_gaa(tree(T44, T45, T46), .(T45, T48), X55)
U4_gaa(T44, T45, T46, T48, X55, preorder_dlB_out_gaa(T44, T48, X54)) → preorder_dlB_out_gaa(tree(T44, T45, T46), .(T45, T48), X55)
U1_ga(T21, T22, T23, T25, preorder_dlB_out_gaa(T21, T25, X26)) → preorder_dlA_out_ga(tree(T21, T22, T23), .(T22, T25))
preorder_dlA_in_ga(tree(T21, T22, T23), .(T22, T25)) → U2_ga(T21, T22, T23, T25, preorder_dlB_in_gaa(T21, T25, T28))
U2_ga(T21, T22, T23, T25, preorder_dlB_out_gaa(T21, T25, T28)) → U3_ga(T21, T22, T23, T25, preorder_dlA_in_ga(T23, T28))
U3_ga(T21, T22, T23, T25, preorder_dlA_out_ga(T23, T28)) → preorder_dlA_out_ga(tree(T21, T22, T23), .(T22, T25))
U7_ga(T5, T7, preorder_dlA_out_ga(T5, T7)) → preorderC_out_ga(T5, T7)
PREORDER_DLB_IN_GAA(tree(T44, T45, T46), .(T45, T48), X55) → U5_GAA(T44, T45, T46, T48, X55, preorder_dlB_in_gaa(T44, T48, T51))
U5_GAA(T44, T45, T46, T48, X55, preorder_dlB_out_gaa(T44, T48, T51)) → PREORDER_DLB_IN_GAA(T46, T51, X55)
PREORDER_DLB_IN_GAA(tree(T44, T45, T46), .(T45, T48), X55) → PREORDER_DLB_IN_GAA(T44, T48, X54)
preorderC_in_ga(T5, T7) → U7_ga(T5, T7, preorder_dlA_in_ga(T5, T7))
preorder_dlA_in_ga(nil, []) → preorder_dlA_out_ga(nil, [])
preorder_dlA_in_ga(tree(T21, T22, T23), .(T22, T25)) → U1_ga(T21, T22, T23, T25, preorder_dlB_in_gaa(T21, T25, X26))
preorder_dlB_in_gaa(nil, T35, T35) → preorder_dlB_out_gaa(nil, T35, T35)
preorder_dlB_in_gaa(tree(T44, T45, T46), .(T45, T48), X55) → U4_gaa(T44, T45, T46, T48, X55, preorder_dlB_in_gaa(T44, T48, X54))
preorder_dlB_in_gaa(tree(T44, T45, T46), .(T45, T48), X55) → U5_gaa(T44, T45, T46, T48, X55, preorder_dlB_in_gaa(T44, T48, T51))
U5_gaa(T44, T45, T46, T48, X55, preorder_dlB_out_gaa(T44, T48, T51)) → U6_gaa(T44, T45, T46, T48, X55, preorder_dlB_in_gaa(T46, T51, X55))
U6_gaa(T44, T45, T46, T48, X55, preorder_dlB_out_gaa(T46, T51, X55)) → preorder_dlB_out_gaa(tree(T44, T45, T46), .(T45, T48), X55)
U4_gaa(T44, T45, T46, T48, X55, preorder_dlB_out_gaa(T44, T48, X54)) → preorder_dlB_out_gaa(tree(T44, T45, T46), .(T45, T48), X55)
U1_ga(T21, T22, T23, T25, preorder_dlB_out_gaa(T21, T25, X26)) → preorder_dlA_out_ga(tree(T21, T22, T23), .(T22, T25))
preorder_dlA_in_ga(tree(T21, T22, T23), .(T22, T25)) → U2_ga(T21, T22, T23, T25, preorder_dlB_in_gaa(T21, T25, T28))
U2_ga(T21, T22, T23, T25, preorder_dlB_out_gaa(T21, T25, T28)) → U3_ga(T21, T22, T23, T25, preorder_dlA_in_ga(T23, T28))
U3_ga(T21, T22, T23, T25, preorder_dlA_out_ga(T23, T28)) → preorder_dlA_out_ga(tree(T21, T22, T23), .(T22, T25))
U7_ga(T5, T7, preorder_dlA_out_ga(T5, T7)) → preorderC_out_ga(T5, T7)
PREORDER_DLB_IN_GAA(tree(T44, T45, T46), .(T45, T48), X55) → U5_GAA(T44, T45, T46, T48, X55, preorder_dlB_in_gaa(T44, T48, T51))
U5_GAA(T44, T45, T46, T48, X55, preorder_dlB_out_gaa(T44, T48, T51)) → PREORDER_DLB_IN_GAA(T46, T51, X55)
PREORDER_DLB_IN_GAA(tree(T44, T45, T46), .(T45, T48), X55) → PREORDER_DLB_IN_GAA(T44, T48, X54)
preorder_dlB_in_gaa(nil, T35, T35) → preorder_dlB_out_gaa(nil, T35, T35)
preorder_dlB_in_gaa(tree(T44, T45, T46), .(T45, T48), X55) → U4_gaa(T44, T45, T46, T48, X55, preorder_dlB_in_gaa(T44, T48, X54))
preorder_dlB_in_gaa(tree(T44, T45, T46), .(T45, T48), X55) → U5_gaa(T44, T45, T46, T48, X55, preorder_dlB_in_gaa(T44, T48, T51))
U4_gaa(T44, T45, T46, T48, X55, preorder_dlB_out_gaa(T44, T48, X54)) → preorder_dlB_out_gaa(tree(T44, T45, T46), .(T45, T48), X55)
U5_gaa(T44, T45, T46, T48, X55, preorder_dlB_out_gaa(T44, T48, T51)) → U6_gaa(T44, T45, T46, T48, X55, preorder_dlB_in_gaa(T46, T51, X55))
U6_gaa(T44, T45, T46, T48, X55, preorder_dlB_out_gaa(T46, T51, X55)) → preorder_dlB_out_gaa(tree(T44, T45, T46), .(T45, T48), X55)
PREORDER_DLB_IN_GAA(tree(T44, T45, T46)) → U5_GAA(T46, preorder_dlB_in_gaa(T44))
U5_GAA(T46, preorder_dlB_out_gaa) → PREORDER_DLB_IN_GAA(T46)
PREORDER_DLB_IN_GAA(tree(T44, T45, T46)) → PREORDER_DLB_IN_GAA(T44)
preorder_dlB_in_gaa(nil) → preorder_dlB_out_gaa
preorder_dlB_in_gaa(tree(T44, T45, T46)) → U4_gaa(preorder_dlB_in_gaa(T44))
preorder_dlB_in_gaa(tree(T44, T45, T46)) → U5_gaa(T46, preorder_dlB_in_gaa(T44))
U4_gaa(preorder_dlB_out_gaa) → preorder_dlB_out_gaa
U5_gaa(T46, preorder_dlB_out_gaa) → U6_gaa(preorder_dlB_in_gaa(T46))
U6_gaa(preorder_dlB_out_gaa) → preorder_dlB_out_gaa
preorder_dlB_in_gaa(x0)
U4_gaa(x0)
U5_gaa(x0, x1)
U6_gaa(x0)
From the DPs we obtained the following set of size-change graphs:
PREORDER_DLA_IN_GA(tree(T21, T22, T23), .(T22, T25)) → U2_GA(T21, T22, T23, T25, preorder_dlB_in_gaa(T21, T25, T28))
U2_GA(T21, T22, T23, T25, preorder_dlB_out_gaa(T21, T25, T28)) → PREORDER_DLA_IN_GA(T23, T28)
preorderC_in_ga(T5, T7) → U7_ga(T5, T7, preorder_dlA_in_ga(T5, T7))
preorder_dlA_in_ga(nil, []) → preorder_dlA_out_ga(nil, [])
preorder_dlA_in_ga(tree(T21, T22, T23), .(T22, T25)) → U1_ga(T21, T22, T23, T25, preorder_dlB_in_gaa(T21, T25, X26))
preorder_dlB_in_gaa(nil, T35, T35) → preorder_dlB_out_gaa(nil, T35, T35)
preorder_dlB_in_gaa(tree(T44, T45, T46), .(T45, T48), X55) → U4_gaa(T44, T45, T46, T48, X55, preorder_dlB_in_gaa(T44, T48, X54))
preorder_dlB_in_gaa(tree(T44, T45, T46), .(T45, T48), X55) → U5_gaa(T44, T45, T46, T48, X55, preorder_dlB_in_gaa(T44, T48, T51))
U5_gaa(T44, T45, T46, T48, X55, preorder_dlB_out_gaa(T44, T48, T51)) → U6_gaa(T44, T45, T46, T48, X55, preorder_dlB_in_gaa(T46, T51, X55))
U6_gaa(T44, T45, T46, T48, X55, preorder_dlB_out_gaa(T46, T51, X55)) → preorder_dlB_out_gaa(tree(T44, T45, T46), .(T45, T48), X55)
U4_gaa(T44, T45, T46, T48, X55, preorder_dlB_out_gaa(T44, T48, X54)) → preorder_dlB_out_gaa(tree(T44, T45, T46), .(T45, T48), X55)
U1_ga(T21, T22, T23, T25, preorder_dlB_out_gaa(T21, T25, X26)) → preorder_dlA_out_ga(tree(T21, T22, T23), .(T22, T25))
preorder_dlA_in_ga(tree(T21, T22, T23), .(T22, T25)) → U2_ga(T21, T22, T23, T25, preorder_dlB_in_gaa(T21, T25, T28))
U2_ga(T21, T22, T23, T25, preorder_dlB_out_gaa(T21, T25, T28)) → U3_ga(T21, T22, T23, T25, preorder_dlA_in_ga(T23, T28))
U3_ga(T21, T22, T23, T25, preorder_dlA_out_ga(T23, T28)) → preorder_dlA_out_ga(tree(T21, T22, T23), .(T22, T25))
U7_ga(T5, T7, preorder_dlA_out_ga(T5, T7)) → preorderC_out_ga(T5, T7)
PREORDER_DLA_IN_GA(tree(T21, T22, T23), .(T22, T25)) → U2_GA(T21, T22, T23, T25, preorder_dlB_in_gaa(T21, T25, T28))
U2_GA(T21, T22, T23, T25, preorder_dlB_out_gaa(T21, T25, T28)) → PREORDER_DLA_IN_GA(T23, T28)
preorder_dlB_in_gaa(nil, T35, T35) → preorder_dlB_out_gaa(nil, T35, T35)
preorder_dlB_in_gaa(tree(T44, T45, T46), .(T45, T48), X55) → U4_gaa(T44, T45, T46, T48, X55, preorder_dlB_in_gaa(T44, T48, X54))
preorder_dlB_in_gaa(tree(T44, T45, T46), .(T45, T48), X55) → U5_gaa(T44, T45, T46, T48, X55, preorder_dlB_in_gaa(T44, T48, T51))
U4_gaa(T44, T45, T46, T48, X55, preorder_dlB_out_gaa(T44, T48, X54)) → preorder_dlB_out_gaa(tree(T44, T45, T46), .(T45, T48), X55)
U5_gaa(T44, T45, T46, T48, X55, preorder_dlB_out_gaa(T44, T48, T51)) → U6_gaa(T44, T45, T46, T48, X55, preorder_dlB_in_gaa(T46, T51, X55))
U6_gaa(T44, T45, T46, T48, X55, preorder_dlB_out_gaa(T46, T51, X55)) → preorder_dlB_out_gaa(tree(T44, T45, T46), .(T45, T48), X55)
PREORDER_DLA_IN_GA(tree(T21, T22, T23)) → U2_GA(T23, preorder_dlB_in_gaa(T21))
U2_GA(T23, preorder_dlB_out_gaa) → PREORDER_DLA_IN_GA(T23)
preorder_dlB_in_gaa(nil) → preorder_dlB_out_gaa
preorder_dlB_in_gaa(tree(T44, T45, T46)) → U4_gaa(preorder_dlB_in_gaa(T44))
preorder_dlB_in_gaa(tree(T44, T45, T46)) → U5_gaa(T46, preorder_dlB_in_gaa(T44))
U4_gaa(preorder_dlB_out_gaa) → preorder_dlB_out_gaa
U5_gaa(T46, preorder_dlB_out_gaa) → U6_gaa(preorder_dlB_in_gaa(T46))
U6_gaa(preorder_dlB_out_gaa) → preorder_dlB_out_gaa
preorder_dlB_in_gaa(x0)
U4_gaa(x0)
U5_gaa(x0, x1)
U6_gaa(x0)
From the DPs we obtained the following set of size-change graphs: